w:World, e:E, t:. isnull(a(loc(e);t))  t<time(e)  {first(e) & ttime(pred(e))} 

latex

Definitions	False, P  Q, A, t  T, {T}, x:A. B(x), SQType(T), Prop, -n, n+m, s ~ t, AB, {x:A| B(x) }, , x:AB(x), b, left+right, P  Q, Dec(P), A & B, a<b, Void, x:AB(x), b, , a(i;t), isnull(a), P & Q, P  Q, Unit, i=j, time(e), pred(e), first(e), loc(e), E, World, ij, #$n, n-m, , s = t
Lemmas	ge wf, nat properties, w-time wf, w-loc wf, w-E wf, world wf, nat wf, not functionality wrt iff, assert of eq int, eq int wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, w-isnull wf, w-a wf, bool wf, bnot wf, not wf, assert wf, false wf, decidable int equal